\begin{tabbing}
(\=Auto$\cdot$) \+
\\[0ex]CollapseTHEN ((All (Unfold `p{-}inject`)) 
\\[0ex]CollapseTHEN ((Auto$\cdot$) 
\\[0ex]CollapseTHEN (
\-\\[0ex](\=(RWO "do{-}apply{-}compose" ({-}1)) \+
\\[0ex]THEN (Auto$\cdot$)$\cdot$) 
\\[0ex]CollapseTHEN (((RepeatFor (first\_nat 2:n
\-\\[0ex])\= ((FLemma `can{-}apply{-}compose` [{-}3]) \+
\\[0ex]CollapseTHENA (Auto$\cdot$)$\cdot$))$\cdot$) 
\\[0ex]CollapseTHEN (((
\-\\[0ex]F\=Hyp 7 [{-}3]) \+
\\[0ex]CollapseTHENA (Auto$\cdot$)$\cdot$) 
\\[0ex]CollapseTHEN ((FHyp 6 [{-}1]) 
\\[0ex]THEN (Auto$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$
\-\\[0ex])$\cdot$)$\cdot$)$\cdot$
\end{tabbing}